<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>InfixDeclaration</title><link rel="stylesheet" href="Agda.css"></head><body><pre><a id="1" class="Background">\documentclass{article}
\usepackage{agda}

\begin{document}

</a><a id="62" class="Markup">\begin{code}</a>
<a id="75" class="Keyword">module</a> <a id="82" href="InfixDeclaration.html" class="Module">InfixDeclaration</a> <a id="99" class="Keyword">where</a>

<a id="106" class="Keyword">infix</a> <a id="112" class="Number">5</a> <a id="114" href="InfixDeclaration.html#130" class="Datatype Operator">_&gt;&gt;_</a> <a id="119" href="InfixDeclaration.html#152" class="Datatype Operator">_&lt;&lt;_</a>

<a id="125" class="Keyword">data</a> <a id="_&gt;&gt;_"></a><a id="130" href="InfixDeclaration.html#130" class="Datatype Operator">_&gt;&gt;_</a> <a id="135" class="Symbol">:</a> <a id="137" class="PrimitiveType">Set</a> <a id="141" class="Keyword">where</a>
<a id="147" class="Keyword">data</a> <a id="_&lt;&lt;_"></a><a id="152" href="InfixDeclaration.html#152" class="Datatype Operator">_&lt;&lt;_</a> <a id="157" class="Symbol">:</a> <a id="159" class="PrimitiveType">Set</a> <a id="163" class="Keyword">where</a>

<a id="170" class="Markup">\end{code}</a><a id="180" class="Background">

Let&#39;s try some infix declaration with surrounding text.

</a><a id="239" class="Markup">\begin{code}</a>
<a id="252" class="Keyword">module</a> <a id="SurroundingText"></a><a id="259" href="InfixDeclaration.html#259" class="Module">SurroundingText</a> <a id="275" class="Keyword">where</a>

<a id="282" class="Markup">\end{code}</a><a id="292" class="Background">

In the following, we declare the fixity of two operators.

</a><a id="353" class="Markup">\begin{code}</a>
  <a id="368" class="Keyword">infix</a> <a id="374" class="Number">5</a> <a id="376" href="InfixDeclaration.html#492" class="Postulate Operator">_+_</a> <a id="380" href="InfixDeclaration.html#496" class="Postulate Operator">_*_</a>
<a id="384" class="Markup">\end{code}</a><a id="394" class="Background">

A fixity declaration can preceed the actual declaration of the names.

</a><a id="467" class="Markup">\begin{code}</a>
  <a id="482" class="Keyword">postulate</a> <a id="SurroundingText._+_"></a><a id="492" href="InfixDeclaration.html#492" class="Postulate Operator">_+_</a> <a id="SurroundingText._*_"></a><a id="496" href="InfixDeclaration.html#496" class="Postulate Operator">_*_</a> <a id="500" class="Symbol">:</a> <a id="502" class="PrimitiveType">Set</a>
<a id="506" class="Markup">\end{code}</a><a id="516" class="Background">

\end{document}
</a></pre></body></html>